(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
0(1(2(3(4(x1))))) → 0(2(1(3(4(x1)))))
0(5(1(2(4(3(x1)))))) → 0(5(2(1(4(3(x1))))))
0(5(2(4(1(3(x1)))))) → 0(1(5(2(4(3(x1))))))
0(5(3(1(2(4(x1)))))) → 0(1(5(3(2(4(x1))))))
0(5(4(1(3(2(x1)))))) → 0(5(4(3(1(2(x1))))))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(2(3(4(z0))))) → 0(2(1(3(4(z0)))))
0(5(1(2(4(3(z0)))))) → 0(5(2(1(4(3(z0))))))
0(5(2(4(1(3(z0)))))) → 0(1(5(2(4(3(z0))))))
0(5(3(1(2(4(z0)))))) → 0(1(5(3(2(4(z0))))))
0(5(4(1(3(2(z0)))))) → 0(5(4(3(1(2(z0))))))
Tuples:
0'(1(2(3(4(z0))))) → c(0'(2(1(3(4(z0))))))
0'(5(1(2(4(3(z0)))))) → c1(0'(5(2(1(4(3(z0)))))))
0'(5(2(4(1(3(z0)))))) → c2(0'(1(5(2(4(3(z0)))))))
0'(5(3(1(2(4(z0)))))) → c3(0'(1(5(3(2(4(z0)))))))
0'(5(4(1(3(2(z0)))))) → c4(0'(5(4(3(1(2(z0)))))))
S tuples:
0'(1(2(3(4(z0))))) → c(0'(2(1(3(4(z0))))))
0'(5(1(2(4(3(z0)))))) → c1(0'(5(2(1(4(3(z0)))))))
0'(5(2(4(1(3(z0)))))) → c2(0'(1(5(2(4(3(z0)))))))
0'(5(3(1(2(4(z0)))))) → c3(0'(1(5(3(2(4(z0)))))))
0'(5(4(1(3(2(z0)))))) → c4(0'(5(4(3(1(2(z0)))))))
K tuples:none
Defined Rule Symbols:
0
Defined Pair Symbols:
0'
Compound Symbols:
c, c1, c2, c3, c4
(3) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)
Removed 5 of 5 dangling nodes:
0'(1(2(3(4(z0))))) → c(0'(2(1(3(4(z0))))))
0'(5(1(2(4(3(z0)))))) → c1(0'(5(2(1(4(3(z0)))))))
0'(5(2(4(1(3(z0)))))) → c2(0'(1(5(2(4(3(z0)))))))
0'(5(3(1(2(4(z0)))))) → c3(0'(1(5(3(2(4(z0)))))))
0'(5(4(1(3(2(z0)))))) → c4(0'(5(4(3(1(2(z0)))))))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(2(3(4(z0))))) → 0(2(1(3(4(z0)))))
0(5(1(2(4(3(z0)))))) → 0(5(2(1(4(3(z0))))))
0(5(2(4(1(3(z0)))))) → 0(1(5(2(4(3(z0))))))
0(5(3(1(2(4(z0)))))) → 0(1(5(3(2(4(z0))))))
0(5(4(1(3(2(z0)))))) → 0(5(4(3(1(2(z0))))))
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
0
Defined Pair Symbols:none
Compound Symbols:none
(5) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(6) BOUNDS(O(1), O(1))